Left Termination of the query pattern
ackermann(g,g,a)
w.r.t. the given Prolog program could successfully be proven:

0 Prolog
↳1 PrologToDTProblemTransformerProof (⇒, 188 ms)
↳2 TRIPLES
↳3 TriplesToPiDPProof (⇒, 176 ms)
↳4 PiDP
↳5 DependencyGraphProof (⇔, 0 ms)
↳6 AND
    ↳7 PiDP
        ↳8 PiDPToQDPProof (⇒, 0 ms)
        ↳9 QDP
        ↳10 QDPSizeChangeProof (⇔, 0 ms)
        ↳11 YES
    ↳12 PiDP
        ↳13 PiDPToQDPProof (⇒, 0 ms)
        ↳14 QDP
        ↳15 QDPSizeChangeProof (⇔, 0 ms)
        ↳16 YES

(0) Obligation:

Clauses:

ackermann(0, N, s(N)).
ackermann(s(M), 0, Val) :- ackermann(M, s(0), Val).
ackermann(s(M), s(N), Val) :- ','(ackermann(s(M), N, Val1), ackermann(M, Val1, Val)).

Query: ackermann(g,g,a)

(1) PrologToDTProblemTransformerProof (SOUND transformation)

Built DT problem from termination graph DT10.

(2) Obligation:

Triples:

ackermannB(X1, X2) :- ackermannC(X1, X2).
ackermannC(s(X1), X2) :- ackermannB(X1, X3).
ackermannC(s(X1), X2) :- ','(ackermanncB(X1, X3), ackermannD(X1, X3, X2)).
ackermannD(s(X1), 0, X2) :- ackermannC(X1, X2).
ackermannD(s(X1), s(X2), X3) :- ackermannD(s(X1), X2, X4).
ackermannD(s(X1), s(X2), X3) :- ','(ackermanncD(s(X1), X2, X4), ackermannD(X1, X4, X3)).
ackermannA(s(s(X1)), 0, X2) :- ackermannB(X1, X3).
ackermannA(s(s(X1)), 0, X2) :- ','(ackermanncB(X1, X3), ackermannA(X1, X3, X2)).
ackermannA(s(X1), s(0), X2) :- ackermannC(X1, X3).
ackermannA(s(X1), s(0), X2) :- ','(ackermanncC(X1, X3), ackermannA(X1, X3, X2)).
ackermannA(s(X1), s(s(X2)), X3) :- ackermannD(s(X1), X2, X4).
ackermannA(s(X1), s(s(X2)), X3) :- ','(ackermanncD(s(X1), X2, X4), ackermannD(X1, X4, X5)).
ackermannA(s(X1), s(s(X2)), X3) :- ','(ackermanncD(s(X1), X2, X4), ','(ackermanncD(X1, X4, X5), ackermannA(X1, X5, X3))).

Clauses:

ackermanncA(0, X1, s(X1)).
ackermanncA(s(0), 0, s(s(0))).
ackermanncA(s(s(X1)), 0, X2) :- ','(ackermanncB(X1, X3), ackermanncA(X1, X3, X2)).
ackermanncA(s(X1), s(0), X2) :- ','(ackermanncC(X1, X3), ackermanncA(X1, X3, X2)).
ackermanncA(s(X1), s(s(X2)), X3) :- ','(ackermanncD(s(X1), X2, X4), ','(ackermanncD(X1, X4, X5), ackermanncA(X1, X5, X3))).
ackermanncB(X1, X2) :- ackermanncC(X1, X2).
ackermanncC(0, s(s(0))).
ackermanncC(s(X1), X2) :- ','(ackermanncB(X1, X3), ackermanncD(X1, X3, X2)).
ackermanncD(0, X1, s(X1)).
ackermanncD(s(X1), 0, X2) :- ackermanncC(X1, X2).
ackermanncD(s(X1), s(X2), X3) :- ','(ackermanncD(s(X1), X2, X4), ackermanncD(X1, X4, X3)).

Afs:

ackermannA(x1, x2, x3)  =  ackermannA(x1, x2)

(3) TriplesToPiDPProof (SOUND transformation)

We use the technique of [DT09]. With regard to the inferred argument filtering the predicates were used in the following modes:
ackermannA_in: (b,b,f)
ackermannB_in: (b,f)
ackermannC_in: (b,f)
ackermanncB_in: (b,f)
ackermanncC_in: (b,f)
ackermanncD_in: (b,b,f)
ackermannD_in: (b,b,f)
Transforming TRIPLES into the following Term Rewriting System:
Pi DP problem:
The TRS P consists of the following rules:

ACKERMANNA_IN_GGA(s(s(X1)), 0, X2) → U9_GGA(X1, X2, ackermannB_in_ga(X1, X3))
ACKERMANNA_IN_GGA(s(s(X1)), 0, X2) → ACKERMANNB_IN_GA(X1, X3)
ACKERMANNB_IN_GA(X1, X2) → U1_GA(X1, X2, ackermannC_in_ga(X1, X2))
ACKERMANNB_IN_GA(X1, X2) → ACKERMANNC_IN_GA(X1, X2)
ACKERMANNC_IN_GA(s(X1), X2) → U2_GA(X1, X2, ackermannB_in_ga(X1, X3))
ACKERMANNC_IN_GA(s(X1), X2) → ACKERMANNB_IN_GA(X1, X3)
ACKERMANNC_IN_GA(s(X1), X2) → U3_GA(X1, X2, ackermanncB_in_ga(X1, X3))
U3_GA(X1, X2, ackermanncB_out_ga(X1, X3)) → U4_GA(X1, X2, ackermannD_in_gga(X1, X3, X2))
U3_GA(X1, X2, ackermanncB_out_ga(X1, X3)) → ACKERMANND_IN_GGA(X1, X3, X2)
ACKERMANND_IN_GGA(s(X1), 0, X2) → U5_GGA(X1, X2, ackermannC_in_ga(X1, X2))
ACKERMANND_IN_GGA(s(X1), 0, X2) → ACKERMANNC_IN_GA(X1, X2)
ACKERMANND_IN_GGA(s(X1), s(X2), X3) → U6_GGA(X1, X2, X3, ackermannD_in_gga(s(X1), X2, X4))
ACKERMANND_IN_GGA(s(X1), s(X2), X3) → ACKERMANND_IN_GGA(s(X1), X2, X4)
ACKERMANND_IN_GGA(s(X1), s(X2), X3) → U7_GGA(X1, X2, X3, ackermanncD_in_gga(s(X1), X2, X4))
U7_GGA(X1, X2, X3, ackermanncD_out_gga(s(X1), X2, X4)) → U8_GGA(X1, X2, X3, ackermannD_in_gga(X1, X4, X3))
U7_GGA(X1, X2, X3, ackermanncD_out_gga(s(X1), X2, X4)) → ACKERMANND_IN_GGA(X1, X4, X3)
ACKERMANNA_IN_GGA(s(s(X1)), 0, X2) → U10_GGA(X1, X2, ackermanncB_in_ga(X1, X3))
U10_GGA(X1, X2, ackermanncB_out_ga(X1, X3)) → U11_GGA(X1, X2, ackermannA_in_gga(X1, X3, X2))
U10_GGA(X1, X2, ackermanncB_out_ga(X1, X3)) → ACKERMANNA_IN_GGA(X1, X3, X2)
ACKERMANNA_IN_GGA(s(X1), s(0), X2) → U12_GGA(X1, X2, ackermannC_in_ga(X1, X3))
ACKERMANNA_IN_GGA(s(X1), s(0), X2) → ACKERMANNC_IN_GA(X1, X3)
ACKERMANNA_IN_GGA(s(X1), s(0), X2) → U13_GGA(X1, X2, ackermanncC_in_ga(X1, X3))
U13_GGA(X1, X2, ackermanncC_out_ga(X1, X3)) → U14_GGA(X1, X2, ackermannA_in_gga(X1, X3, X2))
U13_GGA(X1, X2, ackermanncC_out_ga(X1, X3)) → ACKERMANNA_IN_GGA(X1, X3, X2)
ACKERMANNA_IN_GGA(s(X1), s(s(X2)), X3) → U15_GGA(X1, X2, X3, ackermannD_in_gga(s(X1), X2, X4))
ACKERMANNA_IN_GGA(s(X1), s(s(X2)), X3) → ACKERMANND_IN_GGA(s(X1), X2, X4)
ACKERMANNA_IN_GGA(s(X1), s(s(X2)), X3) → U16_GGA(X1, X2, X3, ackermanncD_in_gga(s(X1), X2, X4))
U16_GGA(X1, X2, X3, ackermanncD_out_gga(s(X1), X2, X4)) → U17_GGA(X1, X2, X3, ackermannD_in_gga(X1, X4, X5))
U16_GGA(X1, X2, X3, ackermanncD_out_gga(s(X1), X2, X4)) → ACKERMANND_IN_GGA(X1, X4, X5)
U16_GGA(X1, X2, X3, ackermanncD_out_gga(s(X1), X2, X4)) → U18_GGA(X1, X2, X3, ackermanncD_in_gga(X1, X4, X5))
U18_GGA(X1, X2, X3, ackermanncD_out_gga(X1, X4, X5)) → U19_GGA(X1, X2, X3, ackermannA_in_gga(X1, X5, X3))
U18_GGA(X1, X2, X3, ackermanncD_out_gga(X1, X4, X5)) → ACKERMANNA_IN_GGA(X1, X5, X3)

The TRS R consists of the following rules:

ackermanncB_in_ga(X1, X2) → U28_ga(X1, X2, ackermanncC_in_ga(X1, X2))
ackermanncC_in_ga(0, s(s(0))) → ackermanncC_out_ga(0, s(s(0)))
ackermanncC_in_ga(s(X1), X2) → U29_ga(X1, X2, ackermanncB_in_ga(X1, X3))
U29_ga(X1, X2, ackermanncB_out_ga(X1, X3)) → U30_ga(X1, X2, ackermanncD_in_gga(X1, X3, X2))
ackermanncD_in_gga(0, X1, s(X1)) → ackermanncD_out_gga(0, X1, s(X1))
ackermanncD_in_gga(s(X1), 0, X2) → U31_gga(X1, X2, ackermanncC_in_ga(X1, X2))
U31_gga(X1, X2, ackermanncC_out_ga(X1, X2)) → ackermanncD_out_gga(s(X1), 0, X2)
ackermanncD_in_gga(s(X1), s(X2), X3) → U32_gga(X1, X2, X3, ackermanncD_in_gga(s(X1), X2, X4))
U32_gga(X1, X2, X3, ackermanncD_out_gga(s(X1), X2, X4)) → U33_gga(X1, X2, X3, ackermanncD_in_gga(X1, X4, X3))
U33_gga(X1, X2, X3, ackermanncD_out_gga(X1, X4, X3)) → ackermanncD_out_gga(s(X1), s(X2), X3)
U30_ga(X1, X2, ackermanncD_out_gga(X1, X3, X2)) → ackermanncC_out_ga(s(X1), X2)
U28_ga(X1, X2, ackermanncC_out_ga(X1, X2)) → ackermanncB_out_ga(X1, X2)

The argument filtering Pi contains the following mapping:
ackermannA_in_gga(x1, x2, x3)  =  ackermannA_in_gga(x1, x2)
s(x1)  =  s(x1)
0  =  0
ackermannB_in_ga(x1, x2)  =  ackermannB_in_ga(x1)
ackermannC_in_ga(x1, x2)  =  ackermannC_in_ga(x1)
ackermanncB_in_ga(x1, x2)  =  ackermanncB_in_ga(x1)
U28_ga(x1, x2, x3)  =  U28_ga(x1, x3)
ackermanncC_in_ga(x1, x2)  =  ackermanncC_in_ga(x1)
ackermanncC_out_ga(x1, x2)  =  ackermanncC_out_ga(x1, x2)
U29_ga(x1, x2, x3)  =  U29_ga(x1, x3)
ackermanncB_out_ga(x1, x2)  =  ackermanncB_out_ga(x1, x2)
U30_ga(x1, x2, x3)  =  U30_ga(x1, x3)
ackermanncD_in_gga(x1, x2, x3)  =  ackermanncD_in_gga(x1, x2)
ackermanncD_out_gga(x1, x2, x3)  =  ackermanncD_out_gga(x1, x2, x3)
U31_gga(x1, x2, x3)  =  U31_gga(x1, x3)
U32_gga(x1, x2, x3, x4)  =  U32_gga(x1, x2, x4)
U33_gga(x1, x2, x3, x4)  =  U33_gga(x1, x2, x4)
ackermannD_in_gga(x1, x2, x3)  =  ackermannD_in_gga(x1, x2)
ACKERMANNA_IN_GGA(x1, x2, x3)  =  ACKERMANNA_IN_GGA(x1, x2)
U9_GGA(x1, x2, x3)  =  U9_GGA(x1, x3)
ACKERMANNB_IN_GA(x1, x2)  =  ACKERMANNB_IN_GA(x1)
U1_GA(x1, x2, x3)  =  U1_GA(x1, x3)
ACKERMANNC_IN_GA(x1, x2)  =  ACKERMANNC_IN_GA(x1)
U2_GA(x1, x2, x3)  =  U2_GA(x1, x3)
U3_GA(x1, x2, x3)  =  U3_GA(x1, x3)
U4_GA(x1, x2, x3)  =  U4_GA(x1, x3)
ACKERMANND_IN_GGA(x1, x2, x3)  =  ACKERMANND_IN_GGA(x1, x2)
U5_GGA(x1, x2, x3)  =  U5_GGA(x1, x3)
U6_GGA(x1, x2, x3, x4)  =  U6_GGA(x1, x2, x4)
U7_GGA(x1, x2, x3, x4)  =  U7_GGA(x1, x2, x4)
U8_GGA(x1, x2, x3, x4)  =  U8_GGA(x1, x2, x4)
U10_GGA(x1, x2, x3)  =  U10_GGA(x1, x3)
U11_GGA(x1, x2, x3)  =  U11_GGA(x1, x3)
U12_GGA(x1, x2, x3)  =  U12_GGA(x1, x3)
U13_GGA(x1, x2, x3)  =  U13_GGA(x1, x3)
U14_GGA(x1, x2, x3)  =  U14_GGA(x1, x3)
U15_GGA(x1, x2, x3, x4)  =  U15_GGA(x1, x2, x4)
U16_GGA(x1, x2, x3, x4)  =  U16_GGA(x1, x2, x4)
U17_GGA(x1, x2, x3, x4)  =  U17_GGA(x1, x2, x4)
U18_GGA(x1, x2, x3, x4)  =  U18_GGA(x1, x2, x4)
U19_GGA(x1, x2, x3, x4)  =  U19_GGA(x1, x2, x4)

We have to consider all (P,R,Pi)-chains

Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES

(4) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

ACKERMANNA_IN_GGA(s(s(X1)), 0, X2) → U9_GGA(X1, X2, ackermannB_in_ga(X1, X3))
ACKERMANNA_IN_GGA(s(s(X1)), 0, X2) → ACKERMANNB_IN_GA(X1, X3)
ACKERMANNB_IN_GA(X1, X2) → U1_GA(X1, X2, ackermannC_in_ga(X1, X2))
ACKERMANNB_IN_GA(X1, X2) → ACKERMANNC_IN_GA(X1, X2)
ACKERMANNC_IN_GA(s(X1), X2) → U2_GA(X1, X2, ackermannB_in_ga(X1, X3))
ACKERMANNC_IN_GA(s(X1), X2) → ACKERMANNB_IN_GA(X1, X3)
ACKERMANNC_IN_GA(s(X1), X2) → U3_GA(X1, X2, ackermanncB_in_ga(X1, X3))
U3_GA(X1, X2, ackermanncB_out_ga(X1, X3)) → U4_GA(X1, X2, ackermannD_in_gga(X1, X3, X2))
U3_GA(X1, X2, ackermanncB_out_ga(X1, X3)) → ACKERMANND_IN_GGA(X1, X3, X2)
ACKERMANND_IN_GGA(s(X1), 0, X2) → U5_GGA(X1, X2, ackermannC_in_ga(X1, X2))
ACKERMANND_IN_GGA(s(X1), 0, X2) → ACKERMANNC_IN_GA(X1, X2)
ACKERMANND_IN_GGA(s(X1), s(X2), X3) → U6_GGA(X1, X2, X3, ackermannD_in_gga(s(X1), X2, X4))
ACKERMANND_IN_GGA(s(X1), s(X2), X3) → ACKERMANND_IN_GGA(s(X1), X2, X4)
ACKERMANND_IN_GGA(s(X1), s(X2), X3) → U7_GGA(X1, X2, X3, ackermanncD_in_gga(s(X1), X2, X4))
U7_GGA(X1, X2, X3, ackermanncD_out_gga(s(X1), X2, X4)) → U8_GGA(X1, X2, X3, ackermannD_in_gga(X1, X4, X3))
U7_GGA(X1, X2, X3, ackermanncD_out_gga(s(X1), X2, X4)) → ACKERMANND_IN_GGA(X1, X4, X3)
ACKERMANNA_IN_GGA(s(s(X1)), 0, X2) → U10_GGA(X1, X2, ackermanncB_in_ga(X1, X3))
U10_GGA(X1, X2, ackermanncB_out_ga(X1, X3)) → U11_GGA(X1, X2, ackermannA_in_gga(X1, X3, X2))
U10_GGA(X1, X2, ackermanncB_out_ga(X1, X3)) → ACKERMANNA_IN_GGA(X1, X3, X2)
ACKERMANNA_IN_GGA(s(X1), s(0), X2) → U12_GGA(X1, X2, ackermannC_in_ga(X1, X3))
ACKERMANNA_IN_GGA(s(X1), s(0), X2) → ACKERMANNC_IN_GA(X1, X3)
ACKERMANNA_IN_GGA(s(X1), s(0), X2) → U13_GGA(X1, X2, ackermanncC_in_ga(X1, X3))
U13_GGA(X1, X2, ackermanncC_out_ga(X1, X3)) → U14_GGA(X1, X2, ackermannA_in_gga(X1, X3, X2))
U13_GGA(X1, X2, ackermanncC_out_ga(X1, X3)) → ACKERMANNA_IN_GGA(X1, X3, X2)
ACKERMANNA_IN_GGA(s(X1), s(s(X2)), X3) → U15_GGA(X1, X2, X3, ackermannD_in_gga(s(X1), X2, X4))
ACKERMANNA_IN_GGA(s(X1), s(s(X2)), X3) → ACKERMANND_IN_GGA(s(X1), X2, X4)
ACKERMANNA_IN_GGA(s(X1), s(s(X2)), X3) → U16_GGA(X1, X2, X3, ackermanncD_in_gga(s(X1), X2, X4))
U16_GGA(X1, X2, X3, ackermanncD_out_gga(s(X1), X2, X4)) → U17_GGA(X1, X2, X3, ackermannD_in_gga(X1, X4, X5))
U16_GGA(X1, X2, X3, ackermanncD_out_gga(s(X1), X2, X4)) → ACKERMANND_IN_GGA(X1, X4, X5)
U16_GGA(X1, X2, X3, ackermanncD_out_gga(s(X1), X2, X4)) → U18_GGA(X1, X2, X3, ackermanncD_in_gga(X1, X4, X5))
U18_GGA(X1, X2, X3, ackermanncD_out_gga(X1, X4, X5)) → U19_GGA(X1, X2, X3, ackermannA_in_gga(X1, X5, X3))
U18_GGA(X1, X2, X3, ackermanncD_out_gga(X1, X4, X5)) → ACKERMANNA_IN_GGA(X1, X5, X3)

The TRS R consists of the following rules:

ackermanncB_in_ga(X1, X2) → U28_ga(X1, X2, ackermanncC_in_ga(X1, X2))
ackermanncC_in_ga(0, s(s(0))) → ackermanncC_out_ga(0, s(s(0)))
ackermanncC_in_ga(s(X1), X2) → U29_ga(X1, X2, ackermanncB_in_ga(X1, X3))
U29_ga(X1, X2, ackermanncB_out_ga(X1, X3)) → U30_ga(X1, X2, ackermanncD_in_gga(X1, X3, X2))
ackermanncD_in_gga(0, X1, s(X1)) → ackermanncD_out_gga(0, X1, s(X1))
ackermanncD_in_gga(s(X1), 0, X2) → U31_gga(X1, X2, ackermanncC_in_ga(X1, X2))
U31_gga(X1, X2, ackermanncC_out_ga(X1, X2)) → ackermanncD_out_gga(s(X1), 0, X2)
ackermanncD_in_gga(s(X1), s(X2), X3) → U32_gga(X1, X2, X3, ackermanncD_in_gga(s(X1), X2, X4))
U32_gga(X1, X2, X3, ackermanncD_out_gga(s(X1), X2, X4)) → U33_gga(X1, X2, X3, ackermanncD_in_gga(X1, X4, X3))
U33_gga(X1, X2, X3, ackermanncD_out_gga(X1, X4, X3)) → ackermanncD_out_gga(s(X1), s(X2), X3)
U30_ga(X1, X2, ackermanncD_out_gga(X1, X3, X2)) → ackermanncC_out_ga(s(X1), X2)
U28_ga(X1, X2, ackermanncC_out_ga(X1, X2)) → ackermanncB_out_ga(X1, X2)

The argument filtering Pi contains the following mapping:
ackermannA_in_gga(x1, x2, x3)  =  ackermannA_in_gga(x1, x2)
s(x1)  =  s(x1)
0  =  0
ackermannB_in_ga(x1, x2)  =  ackermannB_in_ga(x1)
ackermannC_in_ga(x1, x2)  =  ackermannC_in_ga(x1)
ackermanncB_in_ga(x1, x2)  =  ackermanncB_in_ga(x1)
U28_ga(x1, x2, x3)  =  U28_ga(x1, x3)
ackermanncC_in_ga(x1, x2)  =  ackermanncC_in_ga(x1)
ackermanncC_out_ga(x1, x2)  =  ackermanncC_out_ga(x1, x2)
U29_ga(x1, x2, x3)  =  U29_ga(x1, x3)
ackermanncB_out_ga(x1, x2)  =  ackermanncB_out_ga(x1, x2)
U30_ga(x1, x2, x3)  =  U30_ga(x1, x3)
ackermanncD_in_gga(x1, x2, x3)  =  ackermanncD_in_gga(x1, x2)
ackermanncD_out_gga(x1, x2, x3)  =  ackermanncD_out_gga(x1, x2, x3)
U31_gga(x1, x2, x3)  =  U31_gga(x1, x3)
U32_gga(x1, x2, x3, x4)  =  U32_gga(x1, x2, x4)
U33_gga(x1, x2, x3, x4)  =  U33_gga(x1, x2, x4)
ackermannD_in_gga(x1, x2, x3)  =  ackermannD_in_gga(x1, x2)
ACKERMANNA_IN_GGA(x1, x2, x3)  =  ACKERMANNA_IN_GGA(x1, x2)
U9_GGA(x1, x2, x3)  =  U9_GGA(x1, x3)
ACKERMANNB_IN_GA(x1, x2)  =  ACKERMANNB_IN_GA(x1)
U1_GA(x1, x2, x3)  =  U1_GA(x1, x3)
ACKERMANNC_IN_GA(x1, x2)  =  ACKERMANNC_IN_GA(x1)
U2_GA(x1, x2, x3)  =  U2_GA(x1, x3)
U3_GA(x1, x2, x3)  =  U3_GA(x1, x3)
U4_GA(x1, x2, x3)  =  U4_GA(x1, x3)
ACKERMANND_IN_GGA(x1, x2, x3)  =  ACKERMANND_IN_GGA(x1, x2)
U5_GGA(x1, x2, x3)  =  U5_GGA(x1, x3)
U6_GGA(x1, x2, x3, x4)  =  U6_GGA(x1, x2, x4)
U7_GGA(x1, x2, x3, x4)  =  U7_GGA(x1, x2, x4)
U8_GGA(x1, x2, x3, x4)  =  U8_GGA(x1, x2, x4)
U10_GGA(x1, x2, x3)  =  U10_GGA(x1, x3)
U11_GGA(x1, x2, x3)  =  U11_GGA(x1, x3)
U12_GGA(x1, x2, x3)  =  U12_GGA(x1, x3)
U13_GGA(x1, x2, x3)  =  U13_GGA(x1, x3)
U14_GGA(x1, x2, x3)  =  U14_GGA(x1, x3)
U15_GGA(x1, x2, x3, x4)  =  U15_GGA(x1, x2, x4)
U16_GGA(x1, x2, x3, x4)  =  U16_GGA(x1, x2, x4)
U17_GGA(x1, x2, x3, x4)  =  U17_GGA(x1, x2, x4)
U18_GGA(x1, x2, x3, x4)  =  U18_GGA(x1, x2, x4)
U19_GGA(x1, x2, x3, x4)  =  U19_GGA(x1, x2, x4)

We have to consider all (P,R,Pi)-chains

(5) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 2 SCCs with 17 less nodes.

(6) Complex Obligation (AND)

(7) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

ACKERMANNB_IN_GA(X1, X2) → ACKERMANNC_IN_GA(X1, X2)
ACKERMANNC_IN_GA(s(X1), X2) → ACKERMANNB_IN_GA(X1, X3)
ACKERMANNC_IN_GA(s(X1), X2) → U3_GA(X1, X2, ackermanncB_in_ga(X1, X3))
U3_GA(X1, X2, ackermanncB_out_ga(X1, X3)) → ACKERMANND_IN_GGA(X1, X3, X2)
ACKERMANND_IN_GGA(s(X1), 0, X2) → ACKERMANNC_IN_GA(X1, X2)
ACKERMANND_IN_GGA(s(X1), s(X2), X3) → ACKERMANND_IN_GGA(s(X1), X2, X4)
ACKERMANND_IN_GGA(s(X1), s(X2), X3) → U7_GGA(X1, X2, X3, ackermanncD_in_gga(s(X1), X2, X4))
U7_GGA(X1, X2, X3, ackermanncD_out_gga(s(X1), X2, X4)) → ACKERMANND_IN_GGA(X1, X4, X3)

The TRS R consists of the following rules:

ackermanncB_in_ga(X1, X2) → U28_ga(X1, X2, ackermanncC_in_ga(X1, X2))
ackermanncC_in_ga(0, s(s(0))) → ackermanncC_out_ga(0, s(s(0)))
ackermanncC_in_ga(s(X1), X2) → U29_ga(X1, X2, ackermanncB_in_ga(X1, X3))
U29_ga(X1, X2, ackermanncB_out_ga(X1, X3)) → U30_ga(X1, X2, ackermanncD_in_gga(X1, X3, X2))
ackermanncD_in_gga(0, X1, s(X1)) → ackermanncD_out_gga(0, X1, s(X1))
ackermanncD_in_gga(s(X1), 0, X2) → U31_gga(X1, X2, ackermanncC_in_ga(X1, X2))
U31_gga(X1, X2, ackermanncC_out_ga(X1, X2)) → ackermanncD_out_gga(s(X1), 0, X2)
ackermanncD_in_gga(s(X1), s(X2), X3) → U32_gga(X1, X2, X3, ackermanncD_in_gga(s(X1), X2, X4))
U32_gga(X1, X2, X3, ackermanncD_out_gga(s(X1), X2, X4)) → U33_gga(X1, X2, X3, ackermanncD_in_gga(X1, X4, X3))
U33_gga(X1, X2, X3, ackermanncD_out_gga(X1, X4, X3)) → ackermanncD_out_gga(s(X1), s(X2), X3)
U30_ga(X1, X2, ackermanncD_out_gga(X1, X3, X2)) → ackermanncC_out_ga(s(X1), X2)
U28_ga(X1, X2, ackermanncC_out_ga(X1, X2)) → ackermanncB_out_ga(X1, X2)

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
0  =  0
ackermanncB_in_ga(x1, x2)  =  ackermanncB_in_ga(x1)
U28_ga(x1, x2, x3)  =  U28_ga(x1, x3)
ackermanncC_in_ga(x1, x2)  =  ackermanncC_in_ga(x1)
ackermanncC_out_ga(x1, x2)  =  ackermanncC_out_ga(x1, x2)
U29_ga(x1, x2, x3)  =  U29_ga(x1, x3)
ackermanncB_out_ga(x1, x2)  =  ackermanncB_out_ga(x1, x2)
U30_ga(x1, x2, x3)  =  U30_ga(x1, x3)
ackermanncD_in_gga(x1, x2, x3)  =  ackermanncD_in_gga(x1, x2)
ackermanncD_out_gga(x1, x2, x3)  =  ackermanncD_out_gga(x1, x2, x3)
U31_gga(x1, x2, x3)  =  U31_gga(x1, x3)
U32_gga(x1, x2, x3, x4)  =  U32_gga(x1, x2, x4)
U33_gga(x1, x2, x3, x4)  =  U33_gga(x1, x2, x4)
ACKERMANNB_IN_GA(x1, x2)  =  ACKERMANNB_IN_GA(x1)
ACKERMANNC_IN_GA(x1, x2)  =  ACKERMANNC_IN_GA(x1)
U3_GA(x1, x2, x3)  =  U3_GA(x1, x3)
ACKERMANND_IN_GGA(x1, x2, x3)  =  ACKERMANND_IN_GGA(x1, x2)
U7_GGA(x1, x2, x3, x4)  =  U7_GGA(x1, x2, x4)

We have to consider all (P,R,Pi)-chains

(8) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(9) Obligation:

Q DP problem:
The TRS P consists of the following rules:

ACKERMANNB_IN_GA(X1) → ACKERMANNC_IN_GA(X1)
ACKERMANNC_IN_GA(s(X1)) → ACKERMANNB_IN_GA(X1)
ACKERMANNC_IN_GA(s(X1)) → U3_GA(X1, ackermanncB_in_ga(X1))
U3_GA(X1, ackermanncB_out_ga(X1, X3)) → ACKERMANND_IN_GGA(X1, X3)
ACKERMANND_IN_GGA(s(X1), 0) → ACKERMANNC_IN_GA(X1)
ACKERMANND_IN_GGA(s(X1), s(X2)) → ACKERMANND_IN_GGA(s(X1), X2)
ACKERMANND_IN_GGA(s(X1), s(X2)) → U7_GGA(X1, X2, ackermanncD_in_gga(s(X1), X2))
U7_GGA(X1, X2, ackermanncD_out_gga(s(X1), X2, X4)) → ACKERMANND_IN_GGA(X1, X4)

The TRS R consists of the following rules:

ackermanncB_in_ga(X1) → U28_ga(X1, ackermanncC_in_ga(X1))
ackermanncC_in_ga(0) → ackermanncC_out_ga(0, s(s(0)))
ackermanncC_in_ga(s(X1)) → U29_ga(X1, ackermanncB_in_ga(X1))
U29_ga(X1, ackermanncB_out_ga(X1, X3)) → U30_ga(X1, ackermanncD_in_gga(X1, X3))
ackermanncD_in_gga(0, X1) → ackermanncD_out_gga(0, X1, s(X1))
ackermanncD_in_gga(s(X1), 0) → U31_gga(X1, ackermanncC_in_ga(X1))
U31_gga(X1, ackermanncC_out_ga(X1, X2)) → ackermanncD_out_gga(s(X1), 0, X2)
ackermanncD_in_gga(s(X1), s(X2)) → U32_gga(X1, X2, ackermanncD_in_gga(s(X1), X2))
U32_gga(X1, X2, ackermanncD_out_gga(s(X1), X2, X4)) → U33_gga(X1, X2, ackermanncD_in_gga(X1, X4))
U33_gga(X1, X2, ackermanncD_out_gga(X1, X4, X3)) → ackermanncD_out_gga(s(X1), s(X2), X3)
U30_ga(X1, ackermanncD_out_gga(X1, X3, X2)) → ackermanncC_out_ga(s(X1), X2)
U28_ga(X1, ackermanncC_out_ga(X1, X2)) → ackermanncB_out_ga(X1, X2)

The set Q consists of the following terms:

ackermanncB_in_ga(x0)
ackermanncC_in_ga(x0)
U29_ga(x0, x1)
ackermanncD_in_gga(x0, x1)
U31_gga(x0, x1)
U32_gga(x0, x1, x2)
U33_gga(x0, x1, x2)
U30_ga(x0, x1)
U28_ga(x0, x1)

We have to consider all (P,Q,R)-chains.

(10) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • ACKERMANNC_IN_GA(s(X1)) → ACKERMANNB_IN_GA(X1)
    The graph contains the following edges 1 > 1

  • ACKERMANNC_IN_GA(s(X1)) → U3_GA(X1, ackermanncB_in_ga(X1))
    The graph contains the following edges 1 > 1

  • ACKERMANNB_IN_GA(X1) → ACKERMANNC_IN_GA(X1)
    The graph contains the following edges 1 >= 1

  • ACKERMANND_IN_GGA(s(X1), 0) → ACKERMANNC_IN_GA(X1)
    The graph contains the following edges 1 > 1

  • U3_GA(X1, ackermanncB_out_ga(X1, X3)) → ACKERMANND_IN_GGA(X1, X3)
    The graph contains the following edges 1 >= 1, 2 > 1, 2 > 2

  • U7_GGA(X1, X2, ackermanncD_out_gga(s(X1), X2, X4)) → ACKERMANND_IN_GGA(X1, X4)
    The graph contains the following edges 1 >= 1, 3 > 1, 3 > 2

  • ACKERMANND_IN_GGA(s(X1), s(X2)) → ACKERMANND_IN_GGA(s(X1), X2)
    The graph contains the following edges 1 >= 1, 2 > 2

  • ACKERMANND_IN_GGA(s(X1), s(X2)) → U7_GGA(X1, X2, ackermanncD_in_gga(s(X1), X2))
    The graph contains the following edges 1 > 1, 2 > 2

(11) YES

(12) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

ACKERMANNA_IN_GGA(s(s(X1)), 0, X2) → U10_GGA(X1, X2, ackermanncB_in_ga(X1, X3))
U10_GGA(X1, X2, ackermanncB_out_ga(X1, X3)) → ACKERMANNA_IN_GGA(X1, X3, X2)
ACKERMANNA_IN_GGA(s(X1), s(0), X2) → U13_GGA(X1, X2, ackermanncC_in_ga(X1, X3))
U13_GGA(X1, X2, ackermanncC_out_ga(X1, X3)) → ACKERMANNA_IN_GGA(X1, X3, X2)
ACKERMANNA_IN_GGA(s(X1), s(s(X2)), X3) → U16_GGA(X1, X2, X3, ackermanncD_in_gga(s(X1), X2, X4))
U16_GGA(X1, X2, X3, ackermanncD_out_gga(s(X1), X2, X4)) → U18_GGA(X1, X2, X3, ackermanncD_in_gga(X1, X4, X5))
U18_GGA(X1, X2, X3, ackermanncD_out_gga(X1, X4, X5)) → ACKERMANNA_IN_GGA(X1, X5, X3)

The TRS R consists of the following rules:

ackermanncB_in_ga(X1, X2) → U28_ga(X1, X2, ackermanncC_in_ga(X1, X2))
ackermanncC_in_ga(0, s(s(0))) → ackermanncC_out_ga(0, s(s(0)))
ackermanncC_in_ga(s(X1), X2) → U29_ga(X1, X2, ackermanncB_in_ga(X1, X3))
U29_ga(X1, X2, ackermanncB_out_ga(X1, X3)) → U30_ga(X1, X2, ackermanncD_in_gga(X1, X3, X2))
ackermanncD_in_gga(0, X1, s(X1)) → ackermanncD_out_gga(0, X1, s(X1))
ackermanncD_in_gga(s(X1), 0, X2) → U31_gga(X1, X2, ackermanncC_in_ga(X1, X2))
U31_gga(X1, X2, ackermanncC_out_ga(X1, X2)) → ackermanncD_out_gga(s(X1), 0, X2)
ackermanncD_in_gga(s(X1), s(X2), X3) → U32_gga(X1, X2, X3, ackermanncD_in_gga(s(X1), X2, X4))
U32_gga(X1, X2, X3, ackermanncD_out_gga(s(X1), X2, X4)) → U33_gga(X1, X2, X3, ackermanncD_in_gga(X1, X4, X3))
U33_gga(X1, X2, X3, ackermanncD_out_gga(X1, X4, X3)) → ackermanncD_out_gga(s(X1), s(X2), X3)
U30_ga(X1, X2, ackermanncD_out_gga(X1, X3, X2)) → ackermanncC_out_ga(s(X1), X2)
U28_ga(X1, X2, ackermanncC_out_ga(X1, X2)) → ackermanncB_out_ga(X1, X2)

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
0  =  0
ackermanncB_in_ga(x1, x2)  =  ackermanncB_in_ga(x1)
U28_ga(x1, x2, x3)  =  U28_ga(x1, x3)
ackermanncC_in_ga(x1, x2)  =  ackermanncC_in_ga(x1)
ackermanncC_out_ga(x1, x2)  =  ackermanncC_out_ga(x1, x2)
U29_ga(x1, x2, x3)  =  U29_ga(x1, x3)
ackermanncB_out_ga(x1, x2)  =  ackermanncB_out_ga(x1, x2)
U30_ga(x1, x2, x3)  =  U30_ga(x1, x3)
ackermanncD_in_gga(x1, x2, x3)  =  ackermanncD_in_gga(x1, x2)
ackermanncD_out_gga(x1, x2, x3)  =  ackermanncD_out_gga(x1, x2, x3)
U31_gga(x1, x2, x3)  =  U31_gga(x1, x3)
U32_gga(x1, x2, x3, x4)  =  U32_gga(x1, x2, x4)
U33_gga(x1, x2, x3, x4)  =  U33_gga(x1, x2, x4)
ACKERMANNA_IN_GGA(x1, x2, x3)  =  ACKERMANNA_IN_GGA(x1, x2)
U10_GGA(x1, x2, x3)  =  U10_GGA(x1, x3)
U13_GGA(x1, x2, x3)  =  U13_GGA(x1, x3)
U16_GGA(x1, x2, x3, x4)  =  U16_GGA(x1, x2, x4)
U18_GGA(x1, x2, x3, x4)  =  U18_GGA(x1, x2, x4)

We have to consider all (P,R,Pi)-chains

(13) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(14) Obligation:

Q DP problem:
The TRS P consists of the following rules:

ACKERMANNA_IN_GGA(s(s(X1)), 0) → U10_GGA(X1, ackermanncB_in_ga(X1))
U10_GGA(X1, ackermanncB_out_ga(X1, X3)) → ACKERMANNA_IN_GGA(X1, X3)
ACKERMANNA_IN_GGA(s(X1), s(0)) → U13_GGA(X1, ackermanncC_in_ga(X1))
U13_GGA(X1, ackermanncC_out_ga(X1, X3)) → ACKERMANNA_IN_GGA(X1, X3)
ACKERMANNA_IN_GGA(s(X1), s(s(X2))) → U16_GGA(X1, X2, ackermanncD_in_gga(s(X1), X2))
U16_GGA(X1, X2, ackermanncD_out_gga(s(X1), X2, X4)) → U18_GGA(X1, X2, ackermanncD_in_gga(X1, X4))
U18_GGA(X1, X2, ackermanncD_out_gga(X1, X4, X5)) → ACKERMANNA_IN_GGA(X1, X5)

The TRS R consists of the following rules:

ackermanncB_in_ga(X1) → U28_ga(X1, ackermanncC_in_ga(X1))
ackermanncC_in_ga(0) → ackermanncC_out_ga(0, s(s(0)))
ackermanncC_in_ga(s(X1)) → U29_ga(X1, ackermanncB_in_ga(X1))
U29_ga(X1, ackermanncB_out_ga(X1, X3)) → U30_ga(X1, ackermanncD_in_gga(X1, X3))
ackermanncD_in_gga(0, X1) → ackermanncD_out_gga(0, X1, s(X1))
ackermanncD_in_gga(s(X1), 0) → U31_gga(X1, ackermanncC_in_ga(X1))
U31_gga(X1, ackermanncC_out_ga(X1, X2)) → ackermanncD_out_gga(s(X1), 0, X2)
ackermanncD_in_gga(s(X1), s(X2)) → U32_gga(X1, X2, ackermanncD_in_gga(s(X1), X2))
U32_gga(X1, X2, ackermanncD_out_gga(s(X1), X2, X4)) → U33_gga(X1, X2, ackermanncD_in_gga(X1, X4))
U33_gga(X1, X2, ackermanncD_out_gga(X1, X4, X3)) → ackermanncD_out_gga(s(X1), s(X2), X3)
U30_ga(X1, ackermanncD_out_gga(X1, X3, X2)) → ackermanncC_out_ga(s(X1), X2)
U28_ga(X1, ackermanncC_out_ga(X1, X2)) → ackermanncB_out_ga(X1, X2)

The set Q consists of the following terms:

ackermanncB_in_ga(x0)
ackermanncC_in_ga(x0)
U29_ga(x0, x1)
ackermanncD_in_gga(x0, x1)
U31_gga(x0, x1)
U32_gga(x0, x1, x2)
U33_gga(x0, x1, x2)
U30_ga(x0, x1)
U28_ga(x0, x1)

We have to consider all (P,Q,R)-chains.

(15) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • U10_GGA(X1, ackermanncB_out_ga(X1, X3)) → ACKERMANNA_IN_GGA(X1, X3)
    The graph contains the following edges 1 >= 1, 2 > 1, 2 > 2

  • ACKERMANNA_IN_GGA(s(s(X1)), 0) → U10_GGA(X1, ackermanncB_in_ga(X1))
    The graph contains the following edges 1 > 1

  • U16_GGA(X1, X2, ackermanncD_out_gga(s(X1), X2, X4)) → U18_GGA(X1, X2, ackermanncD_in_gga(X1, X4))
    The graph contains the following edges 1 >= 1, 3 > 1, 2 >= 2, 3 > 2

  • U13_GGA(X1, ackermanncC_out_ga(X1, X3)) → ACKERMANNA_IN_GGA(X1, X3)
    The graph contains the following edges 1 >= 1, 2 > 1, 2 > 2

  • U18_GGA(X1, X2, ackermanncD_out_gga(X1, X4, X5)) → ACKERMANNA_IN_GGA(X1, X5)
    The graph contains the following edges 1 >= 1, 3 > 1, 3 > 2

  • ACKERMANNA_IN_GGA(s(X1), s(0)) → U13_GGA(X1, ackermanncC_in_ga(X1))
    The graph contains the following edges 1 > 1

  • ACKERMANNA_IN_GGA(s(X1), s(s(X2))) → U16_GGA(X1, X2, ackermanncD_in_gga(s(X1), X2))
    The graph contains the following edges 1 > 1, 2 > 2

(16) YES